COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.if false then begin "notes"
C00004 00003
C00005 ENDMK
C⊗;
.if false then begin "notes"
1. λ-expressions and λ-conversion
2. statement but not proof of Church-Rosser theorem
3. universality of λ-calculus via simulation of LISP using Scott
devices.
4. remarks including
	just because you can do without explicit conditional expressions
or something else doesn't mean it's practical or even theoretically
preferable  do so
	Church's inconsistent logic
	Scott's models
	lcf
	combinators

	This is more general, but a system that realized it
on a computer would most likely do everything in a more complicated
and slower way for the benefit of rarely utilized generality.  We
say "most likely", because someone may invent a way of getting the
generality without paying any operational penalty.

See lambda.lsp[e80,jmc] for program to normalize λ-expressions
and do pure LISP in λ-calculus.
.end "notes"